\begin{tabbing}
retrace(${\it es}$; $Q$; $X$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E(${\it es}$), ${\it e'}$:es{-}E(${\it es}$). ($Q$($e$,${\it e'}$)) $\Rightarrow$ (($\uparrow$($e$ $\in_{b}$ $X$)) \& ($\uparrow$(${\it e'}$ $\in_{b}$ $X$))))\+
\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;$X$), ${\it e'}$:es{-}E{-}interface(${\it es}$;$X$).\+
\\[0ex]($Q$($e$,${\it e'}$)) $\vee$ ($e$ = ${\it e'}$ $\in$ es{-}E(${\it es}$)) $\vee$ ($Q$(${\it e'}$,$e$)))
\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]$\exists$\=$L$:es{-}E(${\it es}$) List\+
\\[0ex](($\forall$$e$:es{-}E(${\it es}$). ($e$ $\in$ $L$ $\in$ es{-}E(${\it es}$)) $\Leftarrow\!\Rightarrow$ ($Q$($e$,${\it e'}$)))
\\[0ex]\& ($\forall$$e_{1}$:es{-}E(${\it es}$), $e_{2}$:es{-}E(${\it es}$). $e_{1}$ before $e_{2}$ $\in$ $L$ $\in$ es{-}E(${\it es}$) $\Rightarrow$ ($Q$($e_{1}$,$e_{2}$)))))
\-\-\-
\end{tabbing}